As well known, as a model-based development is rising, the importance of a design model in an early development is emphasized over the software industries.
Since a precision of the design model becomes an important factor determining developing costs and time of overall system, it is very important to develop software to analyze whether a written design model is precise.
Further, unified modeling language (hereinafter, referred to as ‘UML’) is a standard language for designing a system model wherein, in UML superstructure specification, a behavior of a system is defined as a behavior within an object and a behavior between objects. The typical diagram representing a behavior within an object is a state machine diagram and the typical diagram representing the behavior between objects is a sequence diagram.
The state machine diagram and the sequence diagram collaborate to define the behavior of a software system. The state machine diagram includes, e.g., a behavioral state machine, a protocol state machine and the like. Specially, since the protocol state machine defines legal transition generated by a class, is not restrained by a specific behavioral construction, and defines legal uses of class, interface, port and the like, the protocol state machine is convenient to describe a life cycle of an object or to define an order of calling operations in a corresponding object. Especially, since the protocol state machine specifies pre-conditions for which operations in an entity is called and post-conditions which are satisfied after the call, the protocol state machine is a very suitable specification to include requirements in the early designing stage of software.
Further, since the sequence diagram is most frequently used to specify scenarios of a system in practices, correspondence analysis between the protocol state machine diagram and the sequence diagram at the early designing stage of software is a very important verification.
In this case, in order to analyze precisely the correspondence between the protocol state machine diagram and the sequence diagram, diagrams are specified using clear formal specification and a formal verification method suitable for a corresponding formal language needs to be used. Model checking is a method of searching all possible cases of specified formal behaviors and is very vigorously used in the field of modern safety engineering.
Bounded model checking (BMC) is a technology proposed to solve the state explosion problem pointed out as disadvantage of the model checking. The BMC is a falsification method of analyzing a system within a certain behavior bound to find an error. The BMC tracks behavior of the system indicating variation of system shapes, e.g., variables, values of the variables and the like up to a restricted range as time goes by to verify whether there is an error. When the BMC denies property of the system and converts the same logically with the system specification while restricting the behavior of the system to K bound, a satisfaction procedure outputs a result called satisfiability and an error scenario, i.e., a model of a system as a basis of the result when there is an error in the bound K. The bound is determined by calculating the maximum number of transmission of messages enabled in the sequence diagram.
In this case, although error is not found by the BMC, it cannot be said there is no error but only there is no error up to a corresponding bound. When an error is found in the corresponding bound, it means that there is an error.
Thus, there is a need for a model checking method of analyzing a software design model, increasing reliability of the analysis results, and automating model checking, like a model checking method for software using the BMC method.